Repository navigation
Harden the finalization and admission carriers; fix CR/NUL escaping in the emitter - #7481
Merged
Merged
Conversation
…n the emitter Follow-up to #7470, addressing its review. Five separable pieces. FINALIZATION CARRIER. WalkPlan is now WalkPlan<F>: gunbc_ci_floor_plan returns WalkPlan<FloorFinalization>, the other three return WalkPlan<NoWalkFinalization>. FloorFinalization moves out of std.realization_schedule to gunbc.ci_materialization, beside the count it is about, so the generic carrier stops owning a growing coproduct of gunbc-specific receipt policies. declared_resolve_count becomes Nat. The review asked for this as a construction wall. It is not one, and the note says so rather than claiming it: probed by execution, substituting NoFinalizationDeclared into the floor while its signature still reads WalkPlan<FloorFinalization> TYPECHECKS and fails only at the first field access. A narrower probe isolates the general defect -- the typechecker does not check a declared return type against the body at all (fn f() -> Int returning a string typechecks), nor a data annotation against its value, while argument position IS checked. So this is a wall-after-grounding whose dissolve-on is return-position typechecking, and the enforcement today is the enrolled witness. require_materialization_disclosure: Bool is deleted. Its false arm skipped the materialization law while the success line still reported that disclosure held -- a writable bypass with a lie attached, pre-authored for a consumer that does not exist. Disclosure is intrinsic to FloorFinalization now. FINALIZATION WITNESSES. Two rows that execute: the floor projects ci_floor_declared_resolve_count, and a forked-by-one count is refused by the same predicate. The other four the review listed are not written, deliberately: matching a one-inhabitant type returns true for every input. ATTEMPT SUBJECT. WalkAttemptId is a PathSegment brand with one constructor, testing std.types.path_segment_is_safe -- the single authority for what makes a string safe to concatenate as a path segment. ../other-attempt, a/b, ".", "..", backslash, CR, LF and NUL now refuse through BOTH producers. The v2 wire parsers require EXACT arity (5 / 6 / 7 lines) and route every required field through its domain constructor; a seventh line that is not an integer refuses the whole receipt instead of becoming pr_number: none. The gate consumes the CAPTURED subject, not a self-describing receipt: tested_head_sha was carried and never read, so a receipt could restate which subject it certified and be believed. Three bindings precede any freshness question, and a mismatch is MergeDeniedSubjectMismatch, its own state. The tested base tree grounds on the existing extdeps.git.object_store.GitObjectId rather than ContentHash, which DESIGN already records as one brand over two unrelated hash families. EMITTER, CR AND NUL. escape_string_literal_body split on the delimiter "\r", but this language's tokenizer has no \r escape -- its table is \" \\ \n \t \{ \} and \xHH -- so that delimiter was the two characters backslash and r, and carriage returns have passed through unescaped into every emitted target for as long as the function has existed. Dead in practice only because no corpus string carried one; the first that did turned it into a hard emit failure. Fixed in the .dag authority and the seed, with NUL added beside it. Regen is a fixed point over two runs. Also: the duplicate unreachable MergeDeniedWrongAttempt arm, and the stale diagnostics that still described finalization as read from the plan closure at arm time or the WalkPlan record as { batches, on_success_stages }. A resolve-count mismatch now locates itself at <entry>::<function> WalkPlan.finalization.declared_resolve_count rather than always pointing at the production authority. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01N7LfCpidMuDjV3FxYUHv1K
…ed object ids, cross-target escapes
Six items from the review, plus the CI floor failure the first head hit.
THE CI FAILURE, first, because it is the one defect rather than a refinement.
`claim_executor: WalkPlan.finalization: must be a NoFinalizationDeclared or
FloorFinalization value, got FloorFinalization { declared_resolve_count: 1 }`. Moving
FloorFinalization out of the WalkFinalization sum into a standalone record changed its
RUNTIME shape from Value::Variant to Value::Record, and the parser only matched
variants. The .dag witnesses stayed green throughout because field access works fine on
a record -- the executor's parser was never executed against the new shape, which is
exactly the specification-without-execution trap. Both shapes are matched now, by TYPE
NAME rather than by "has a field called declared_resolve_count", and the repair is
proven by running claim_executor against the budget RED-control fixture: "floor contract
finalized -- resolve count matches declared 1 and materialization disclosure holds".
1. Every residual construction-wall overclaim is gone. floor_finalization_note,
walk_plan_uniformity_note, the RED fixture's note and two seed doc comments all said the
signature rejects the empty policy or that plans cannot acquire the laws by picking a
value. They now say what is true: WalkPlan<F> DECLARES the intended family and removes
the std-level coproduct fork; the enrolled value witnesses and the runtime parser are the
wall until return-position typechecking lands.
2. The three no-finalization witnesses are added, and the reasoning that omitted them was
wrong. It assumed the declared return type bounds the runtime value; the probe shows it
does not, so matching the actual value is load-bearing rather than a match over a
one-inhabitant type. regen, plan-artifact and falsifier each carry NoFinalizationDeclared,
witnessed.
3. The duplicate MergeDeniedSubjectMismatch arm is deleted -- the same residue class as
the duplicate WrongAttempt arm this branch already removed, reintroduced by the mechanical
pass that added the new variant.
4. Git object ids are now VALIDATED, not merely branded. git_sha1_object_id /
git_sha256_object_id land beside GitObjectId in extdeps.git.object_store, checking exact
length (40/64) and canonical lowercase hex through the existing
git_decode_lower_hex_octets rather than a second hex reader. Before this, sha1:x,
sha1:not-hex and a 64-digit value labelled sha1 all parsed: family without length and
syntax is not identification. git_object_id_eq moves there too -- it is generic Git
behaviour and holding it in the admission consumer was a fork. Seven REDs.
5. The escape replacement was itself target-specific. Fixing the CR DELIMITER was only
half: emitting \r and \0 is Rust-shaped, and escape_string_literal_body is
target-independent -- emit_string_literal invokes it for Rust, Dag, Go and Python alike
and never sees a RenderTarget -- so \r into a Dag literal reproduces the exact
backslash-r bug the delimiter half just fixed. The spelling is \x0d and \x00, the hex
form all four grammars accept. Proven by an inverse-pair round trip through the
tokenizer's own process_escapes, with a control asserting the characters are actually
replaced (identity round-trips perfectly). Rust is proven by compilation; Go and Python
are NOT proven and the test says so -- no toolchain here, no modeled escape grammar,
dissolve-on named.
Also: path_segment_is_safe is a predicate rather than a constructor, so std holds the law
and each brand constructs itself through it -- a generic constructor would put the
branding cast in std, where the emitter cannot render it, and every caller would re-cast
into its own brand anyway.
Not fixed here, recorded: cargo build fails on the v1-stage0-std-core crate at this
branch's merge base too (7 errors, unresolved extdeps_units_* / std_occurrence_identity
imports), and compiler_tests::rust_btree_set_ord_eligibility_requires_nominal_carrier_shape
was already red before these changes. Neither is caused by this PR.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01N7LfCpidMuDjV3FxYUHv1K
…id equality from its definer
The floor's compile-clean gate reported one hard diagnostic:
dag/tools/merge_admission_gate.dag:28:3: error: non-exhaustive match:
missing variant(s) MergeDeniedSubjectMismatch
Adding MergeDeniedSubjectMismatch to MergeAdmissionVerdict obligates every total match
over it, and one consumer was missed. The miss is the same shape as the false
"zero consumers" claim earlier in this arc: the census searched dag/gunbc, dag/test/claim
and src/v2 and never looked in dag/tools, so the one consumer outside those three was
invisible to it. The re-census is whole-tree and untruncated, and finds exactly four
consumers, all now exhaustive.
Two process corrections behind this, since the same class has now cost three round trips:
- The exhaustiveness check is doing its job. Adding a variant SHOULD break every total
match; that is the fail-closed behaviour, and the defect is entirely in the census
that failed to enumerate them.
- Local verification was narrower than CI twice over. Witness-closure runs resolve only
each entry's own imports, so a consumer in an unrelated subtree is never compiled.
This change was verified by running the same whole-tree `--target dag` compile the
gate runs, which is green.
Also: the attempt witness imported git_object_id_eq through gunbc.merge_admission, which
re-exports it, rather than from extdeps.git.object_store where it is defined. Import from
the definer -- a re-export chain is the shape DESIGN's import-strip cascade diagnosis
names as resolving by pool-membership coincidence.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01N7LfCpidMuDjV3FxYUHv1K
…onsumer obsoleted The floor reached the witness corpus and one row of 5498 failed: inert_carrier_no_unrostered_or_stale (src/v2/lens/inert_carrier_test.dag) Bisected by execution: 1 STALE roster entry, 0 unrostered, and the stale one is FilePermissions. The cause is not in this PR. main's aaa3e8a added dag/gunbc/managed_directory.dag, which consumes FilePermissions to derive a directory mode from its declared dependents, and that module's own note states the consequence it did not carry out -- "it is named on the inert-carrier roster (v2.lens.inert_carrier) for exactly that reason, and this module is the live consumer that takes it off, the same way RbacPolicy came off when extdeps/bmc/access.dag started using it". The row is deleted here because this PR is the next one to merge main, and it blocks on it. The ratchet worked; the PR that should have tripped it never ran it. Both RED controls in that witness file stay green (count_not_in_roster_detects_unrostered, count_stale_roster_detects_stale_entry), so the mechanism still discriminates rather than having been quieted. WHY MAIN MERGED RED, recorded because the roster row is the symptom and this is the defect. src/v2/lens/inert_carrier_test.dag declares live_tree_disposition: SubstrateInputsOnly, but its verdict comes from inert_carrier_names_live() -- a host builtin that walks the whole corpus on disk (build_inert_carrier_data, cli_run.rs:27382). Its inputs are therefore NOT its import closure, and managed_directory.dag is not in that closure, so affected-set selection on a .dag-only diff will not select the one witness whose entire job is to notice that diff. CI's own note names the right treatment -- "ReadsLiveTree rows (doc-graph wall, corpus-read host-fed lenses) always run" -- and this is a corpus-read host-fed lens declared as substrate-inputs-only. The disposition is NOT changed here. Making it always-run is a per-PR cost decision of the same class as a declared-resolve-count bump, it belongs to the affected-set lane rather than to a carrier-hardening PR, and the scheduled falsifier is designed to surface exactly this as a counted divergence within one cadence window -- so the question of whether that already fired and went unread should be answered before adding standing cost. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01N7LfCpidMuDjV3FxYUHv1K
briansrls
marked this pull request as ready for review
July 31, 2026 02:44
|
Bugbot is not enabled for your account, so this pull request was not reviewed. Enable Bugbot in the Cursor dashboard to get automatic reviews on future PRs. |
gunbai-bot Bot
pushed a commit
that referenced
this pull request
Jul 31, 2026
Integrate merge-admission hardening from #7481 (WalkAttemptId, subject-binding gate, wire-format validation) with the ContentHash family-grounding lane on this branch. Co-authored-by: Cursor <cursoragent@cursor.com>
gunbai-bot Bot
pushed a commit
that referenced
this pull request
Jul 31, 2026
… merge
TWO defects, one found by review and one by the merge.
MISSING SEPARATOR (claude review 45347, correct). The `count` row added to
`partial_function_templates` was not comma-separated from the `length` row
above it, so two record literals sat adjacent inside the list. Fixed.
The reason it survived is worth recording, because it is the same class this
PR is about: THE PARSER SILENTLY ACCEPTS A MISSING LIST SEPARATOR. Probed
directly — `[ { name: "a" }, { name: "b" } { name: "c" } ]` compiles with 0
diagnostics. So the malformed literal passed regen, a whole-corpus compile,
the fixed-point verify, and a 15-case control matrix without a murmur, and
`Map |> count` resolved green off it. No amount of execution would have caught
this; it took someone reading the diff. A grammar that accepts juxtaposed
elements cannot tell a two-element list from a three-element one, which makes
a dropped comma a silent semantic change — unowned, and named here.
STALE SEED AFTER THE MERGE. Merging origin/main brought #7481, which added
literal CR/NUL characters to dag/std/types.dag AND the emitter fix that
escapes them (\x0d / \x00, target-independent). The merge kept my side of the
seed, which predates that fix, so the committed stage0 could no longer emit
the .dag it is derived from: `regen_stage0 --verify` failed with "bare CR not
allowed in string" in a freshly emitted std_types.rs. Authority and seed had
diverged — precisely the drift the regen gate exists to catch, caught.
Re-derived by bootstrapping from main's seed (which carries the escaping fix)
and running the two-pass regen, rather than by hand-patching the seed.
Re-verified after both fixes, not assumed:
regen_stage0 --verify regen_divergence_count=0
control matrix 6 REDs; positive controls 0 diagnostics
witnesses method_existence_wall_witness ok,
declared_type_conformance_witness ok
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
briansrls
pushed a commit
that referenced
this pull request
Aug 1, 2026
* WIP: p0 - protect the live system
* Refuse an unresolved method instead of inheriting the receiver type
An unknown method reached `method_pipe_map_keys_values_fallback`'s else-arm,
which returned the RECEIVER's type with an empty diagnostic list. So
`xs |> filter_map(..)` on a `List<Int>` typed as another `List<Int>` — a
success-shaped answer that survives a whole collection pipeline and looks
plausible to downstream inference, with the expression stamped
`PlainMethodSemantics` as if it had resolved. Nothing refused until the
interpreter hit its closed dispatch default and returned
`InterpError::Unimplemented { what: "method 'filter_map'" }`: whole-tree
compile reported zero blocking errors while live dispatch returned HTTP 500
(#7479).
That arm is deleted. Method absence is now decided at compile time and split
into the two states it actually has (DESIGN §5 — state-space conflation):
MethodNotFound receiver type fully resolved, so the method is
PROVABLY absent — the decidable refusal.
MethodExistenceUndecided receiver under-resolved (type variables present),
so absence cannot be proven — a typed, located,
COUNTED frontier refusal, never a silent widen
back to `recv_rt`.
Both arms return `error_type`, not `recv_rt`: `node_type_compatible` treats
`error_type` as compatible with everything, so one located refusal does not
cascade into derived mismatches at every downstream consumer.
Green by execution, with the controls:
xs |> deliberately_nonexistent_method() RED, names method + receiver type
xs |> filter_map(x => x) RED — the literal #7479 incident
xs |> filter(..) |> map(..) GREEN — algebra templates resolve
at tier0 and never reach the arm
Rationale rides on the carrier (`method_existence_wall_note`) with its
dissolve-on: primitive-realization-single-authority, at which point existence
is decided against one PrimitiveDefinition identity rather than the
structural/service tier pair, and the Undecided frontier closes.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
* WIP: p0 - protect the live system
* Decide method existence and declared-type conformance at compile time
Two v1 fail-opens in the same shape: knowledge is missing, so the compiler
constructs a success-shaped answer and the lie surfaces at runtime.
METHOD EXISTENCE. An unresolved method fell through
`method_pipe_map_keys_values_fallback`'s else-arm, which returned the
RECEIVER's type with an empty diagnostic list, and the expression was stamped
`PlainMethodSemantics` as if it had resolved. So `xs |> filter_map(..)` on a
`List<Int>` typed as another `List<Int>` and survived the whole pipeline;
nothing refused until `InterpError::Unimplemented { what: "method
'filter_map'" }` — whole-tree compile green, live dispatch HTTP 500 (#7479).
The predicate deciding absence is the load-bearing part, and the two obvious
ones are unsound — both rejected on measured whole-tree evidence, not taste:
is_fully_resolved alone A type can carry no type variables and still be
an inference artifact. `NonEmptyStr` (declared
`String where non_empty`) arrives as
Product(NonEmptyStr) instead of peeling to its
String base, reding 8 correct `.length()` sites
in extdeps/filesystem/linux.dag while the
identical `text.length()` in extdeps/mercurial
stays green; a coproduct payload bound by
pattern destructuring arrives typed
Primitive(ok) and reds a correct `list_push`.
the receiver algebra profile free_monoid_scalar_templates omits `count`
while the interpreter dispatches it natively,
so `String.count()` reds against a profile the
runtime contradicts — the five-way primitive
fork, measured.
Fabricating a refusal is the mirror image of the fabricated success being
deleted, so the predicate is composed of two declared authorities rather than
one minted here: refuse when the name is absent from `std.methods`
declared_method_names AND the receiver is fully resolved. The roster answers
"is this a substrate method at all"; the receiver gate answers "could this be
a product field holding a callable" — exactly the legitimate
`LexMatchThunk { apply: fn(s) }` idiom in v2's tokenizer, whose 7 sites would
red without it. Whole-corpus verdict: zero false positives, and a second real
latent defect caught beside #7479 — `env.clone()` (05_emit_rust.dag:9009,9831),
a Rust-ism with no .dag definition and no interpreter arm, fixed here.
The undecidable residue is `MethodExistenceUndecided`: typed, located and
COUNTED but non-blocking (the is_error_diagnostic partition, UnlistedImportUse
precedent), so the frequency of the frontier stays observable rather than
zeroed by construction. Both arms return error_type, never recv_rt, so one
located refusal does not cascade downstream.
DECLARED-TYPE CONFORMANCE. infer_item passed the declared return into body
inference as `expected` but then kept the declaration's inferred return
regardless of what the body produced, so `fn f() -> Int { "wrong" }`
typechecked with zero diagnostics. Three positions now check against their
declaration — fn body vs declared return (both arms) and `data` value vs
annotation — through the EXISTING node_type_compatible, which is permissive by
design: an error type, type variable, or under-resolved shape answers
compatible, so the wall fires only where the mismatch is proven.
Green by execution. REDs: `deliberately_nonexistent_method`, `filter_map`,
`fn f() -> Int { "a string" }`, `data d: Int = "a string"`. GREENs:
filter/map/fold/flat_map pipelines, `String |> count`, `Int?` from `first`,
and the full [src/v1, dag] closure through regen.
Two upstream defects are named by the measurement and deliberately not fixed
here, each a promotion trigger that would let the wall decide more: a
where-refinement alias resolving to a Product instead of peeling to its base,
and a coproduct payload binding typed as the variant name.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
* Narrow the conformance wall to what it can actually prove
The method-existence wall landed sound. The declared-type conformance wall
did not: running it over the corpus found FOUR independent classes of correct
code that node_type_compatible reports as a mismatch, because it compares
names across representations it never peels.
optionality, two ways `-> String?` carries optionality in
return_cardinality while the body produces the
nominal Optional coproduct — 4 correct sites in
05_emit_rust.dag
brand aliases `Hash` is `ContentHash` is a branded String — 3
correct sites in dag_collect_support.dag, the same
class as NonEmptyStr arriving as Product(NonEmptyStr)
anonymous literals the corpus writes `[ { name: .., .. } ]` without
repeating the nominal type — 8+ correct rows in
dag/std/algebra.dag
cardinality location resolved_type() drops the declaration's optional
marker (fixed: the declared side now goes through
preserve_outer_optional_cardinality)
Each was found by RUNNING the wall, never by reasoning about it, and the list
is not known to be exhaustive — which is exactly why chasing them with
exemptions was the wrong move. Four ad-hoc carve-outs leave a wall that is
neither principled nor trustworthy, and fabricating a refusal is the mirror
image of the fabricated success the wall exists to delete.
So conformance uses the same predicate shape the method wall settled on:
positive establishment. Judge only when both sides are ground kernel scalars —
plain shape, Required cardinality, name in std.types kernel_type_set — because
then a name difference IS a real difference, with no alias, brand, container,
coproduct or cardinality representation in between. That admits the whole class
the report named and admits nothing it cannot prove. Everything wider is
UNJUDGED rather than silently passed: it is the wall's declared frontier, and
each class above is a promotion trigger carried on the carrier note.
Witnesses are enrolled and executing, not scratchpad probes:
method_existence_wall_witness and declared_type_conformance_witness in the
emitted compiler_tests, both green, both discriminating (the asserted
diagnostic lists were empty before the walls).
4 REDs deliberately_nonexistent_method · filter_map · fn f() -> Int
{ "a string" } · data d: Int = "a string"
8 GREEN filter/map/fold/flat_map pipelines · String |> count · Int? from
first · conforming returns and data
regen_stage0 --verify: regen_divergence_count=0 — committed stage0 matches a
fresh self-compile, so the seed is at its fixed point with both walls active.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
* WIP: p0 - protect the live system
* chore: regenerate drifted generated artifacts (ci auto-heal)
* WIP: p0 - protect the live system
* Restore the seed the auto-WIP commit stripped
7b0ecdd8ea ("WIP: p0 - protect the live system") captured my working tree
mid-experiment and committed it. The tree at that moment held a deliberately
reverted seed: I had checked out the pre-wall stage0 to run a CONTROL — to
establish whether the OOM in
module_grain_affected_decision_discriminates_under_wiring_perturbation was
caused by this PR or pre-existing. (It is pre-existing: the test is SIGKILLed
identically on the pre-wall seed with 101 GB free, consistent with the repo's
own "whole-tree resolve OOM risk in test harness" note.)
The commit therefore deleted the walls from the seed while leaving them in the
.dag authority: 300 deletions across v1_std_core.rs (both diagnostic variants),
v1_compiler_infer.rs (the composed predicate and the conformance gate),
cli_run.rs (the histogram arms), compiler_tests.rs (both witnesses), and
lib.rs (the std_methods module). That is the exact drift the regen gate exists
to catch, and it was pushed.
The seed is restored byte-identical to 2b4380df3c ("chore: regenerate drifted
generated artifacts"), the last state where authority and seed agreed.
Re-verified after restore, not assumed:
regen_stage0 --verify regen_divergence_count=0 — committed stage0 matches a
fresh self-compile
control matrix 4 REDs (deliberately_nonexistent_method, filter_map,
fn f() -> Int { "a string" }, data d: Int =
"a string"), 8 positive controls green
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
* Decide method existence per receiver, not per name (codex review 45327)
The review is correct, and confirmed by execution. Gating on membership in a
declared method-NAME roster admits any rostered name on ANY receiver, so:
fn g(xs: List<Int>) -> Bool { xs |> starts_with("x") } compiled clean
fn h(xs: List<Int>) -> String { xs |> to_upper() } compiled clean
Both landed in MethodExistenceUndecided, which is non-blocking, so
`emittable_graph` accepted them — a fail-open route to exactly the runtime
failure this P0 wall exists to remove. Worse, the diagnostic LIED about its
cause: it reported the receiver as "under-resolved" when
Container(List,Primitive(Int)) is fully resolved. I had also reported
`String |> count` as a passing positive control; it was passing through this
same hole and emitting an advisory, so that green was hollow.
The predicate is now PER-RECEIVER: refuse when kernel_profile_lookup returns a
profile for the receiver's canonical container kind. tier0 has already
consulted that profile's algebra templates and missed, so reaching this arm
with a kernel-profiled receiver PROVES absence from the receiver's complete
declared surface. Same authority tier0 reads; no second relation.
That predicate was blocked by ONE thing, and it is a real §3 fork now fixed
rather than worked around: the kernel profiles disagreed with the interpreter
about `count`. The interpreter dispatches "length" | "count" | "size" natively,
while free_monoid_scalar_templates (String) and partial_function_templates
(Map) declared only `length`. Measured over the whole [src/v1, dag] closure the
gap was exactly two shapes — String |> count and Map |> count (9 sites) — and
both profiles now declare `count`, mirroring their own `length` row. So those
calls resolve at tier0 and never reach the wall.
Non-kernel receivers stay Undecided, and refusing there WOULD fabricate: a
where-refinement alias arrives as Product(NonEmptyStr) rather than peeling to
String, a coproduct payload arrives typed Primitive(ok), and `apply` is a
product FIELD holding a callable (the LexMatchThunk idiom). Undecided now means
exactly one thing — receiver surface not established — instead of doubling as a
name-grain escape hatch.
The name roster added in the previous commit is deleted along with its
generated module and registry row: the per-receiver predicate does not consult
it, and an unused authority is dead scaffolding.
6 REDs deliberately_nonexistent_method · filter_map · starts_with · to_upper
· fn f() -> Int { "a string" } · data d: Int = "a string"
9 GREEN 0 diagnostics, not merely no MethodNotFound — incl. String |> count
and Map |> count, now genuinely resolved rather than fail-open
The witness carries the review's two cases as REDs, so a regression to a
name-grain predicate fails the test rather than passing it.
regen_stage0 --verify: regen_divergence_count=0.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
* Fix the missing list separator, and re-derive the seed after the main merge
TWO defects, one found by review and one by the merge.
MISSING SEPARATOR (claude review 45347, correct). The `count` row added to
`partial_function_templates` was not comma-separated from the `length` row
above it, so two record literals sat adjacent inside the list. Fixed.
The reason it survived is worth recording, because it is the same class this
PR is about: THE PARSER SILENTLY ACCEPTS A MISSING LIST SEPARATOR. Probed
directly — `[ { name: "a" }, { name: "b" } { name: "c" } ]` compiles with 0
diagnostics. So the malformed literal passed regen, a whole-corpus compile,
the fixed-point verify, and a 15-case control matrix without a murmur, and
`Map |> count` resolved green off it. No amount of execution would have caught
this; it took someone reading the diff. A grammar that accepts juxtaposed
elements cannot tell a two-element list from a three-element one, which makes
a dropped comma a silent semantic change — unowned, and named here.
STALE SEED AFTER THE MERGE. Merging origin/main brought #7481, which added
literal CR/NUL characters to dag/std/types.dag AND the emitter fix that
escapes them (\x0d / \x00, target-independent). The merge kept my side of the
seed, which predates that fix, so the committed stage0 could no longer emit
the .dag it is derived from: `regen_stage0 --verify` failed with "bare CR not
allowed in string" in a freshly emitted std_types.rs. Authority and seed had
diverged — precisely the drift the regen gate exists to catch, caught.
Re-derived by bootstrapping from main's seed (which carries the escaping fix)
and running the two-pass regen, rather than by hand-patching the seed.
Re-verified after both fixes, not assumed:
regen_stage0 --verify regen_divergence_count=0
control matrix 6 REDs; positive controls 0 diagnostics
witnesses method_existence_wall_witness ok,
declared_type_conformance_witness ok
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
* WIP: p0 - protect the live system
* Make the positive controls assert zero diagnostics (codex review 45357)
The review's second finding is correct: both witnesses filtered the green
module's diagnostics to the BLOCKING variant only (MethodNotFound /
TypeMismatch), so an advisory MethodExistenceUndecided passed unnoticed.
That is not hypothetical — it is exactly how I came to report `String |> count`
as a passing positive control when it was in fact resolving through the
non-blocking arm and emitting an advisory. The witness was structurally unable
to tell "this call resolves" from "this call does not resolve but the arm is
advisory", which is the whole distinction the wall turns on.
Both controls now assert `green_result.diagnostics.is_empty()` — no diagnostic
of any severity. A legitimate method that stops resolving, or a conforming
declaration that starts producing an advisory, now fails the witness instead of
passing it.
Verified: both witnesses green under the strengthened assertion, so the
positive controls demonstrably resolve rather than being admitted by an arm.
regen_stage0 --verify: regen_divergence_count=0.
The review's first finding — that MethodExistenceUndecided is non-blocking, so
emittable_graph still emits — is answered separately on the PR with the
measured site list, because the fix is not available in this PR: 7 of the
Undecided sites are the v2 tokenizer's own LexMatchThunk { apply: fn(s) }
idiom, so blocking today refuses the compiler v2 depends on.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
* Remove a foreign PR's Rust slice that a bootstrap checkout dragged in
Bootstrapping the seed required a compiler that could emit the merged .dag, so
I ran `git checkout origin/main -- src/v1/stage0/src/`. origin/main had
advanced past this branch's merge base (da37e37f9b) to b519142647, so that
path-scoped checkout imported the stage0 slice of #7483 ("Exclusive cost
partition + selected-set closure overlap") — its hand-maintained bins — while
leaving the rest of that PR behind.
The result was four files in this diff that are not this PR's work:
measure_selected_closure_overlap.rs (a new file, and orphaned — Cargo.toml at
this branch's base does not declare the bin, so nothing built it), plus edits
to claim_batch.rs, claim_executor.rs and measure_whole_tree_resolve.rs.
Half of someone else's merged change, presented as mine, is not something to
carry to review: it misattributes the work and it is a partial import whose
.dag half is absent. All four are restored to the merge base; main's own
versions land normally when this branch merges.
Caught by reading the diff surface after a reviewer's summary described "two
new measurement bins" I had not written — a reminder that a path-scoped
checkout against a moving ref imports whatever else has landed there.
Verified after the strip: cargo build clean, regen_stage0 --verify
regen_divergence_count=0.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
* WIP: p0 - protect the live system
* WIP: p0 - protect the live system
* Peel the refinement base so the wall DECIDES, and key the frontier on receiver shape
Two independent signals said the same thing about the (module, method)
frontier key: codex review 45398 found it as a fail-open (a NEW `apply` in
v2.compiler.tokenize inherited the pass on any receiver, so the note's claim
that no new fail-open could enter was false), and the first whole-corpus CI run
found it as an undercount — the roster was measured over the v1 self-compile
closure alone and seven sites in three unseen modules went red.
The larger finding is that the biggest "undecidable" class was never
undecidable. resolve_method_receiver_type short-circuits on connective == Conj,
and a where-refinement type IS a Conj, so `String where non_empty` reached
method lookup as Product(NonEmptyStr) and String's algebra profile was never
consulted. Peeling to the base moves 12 corpus sites out of the residue in both
directions at once: the correct `.length()` calls resolve, AND a method genuinely
absent from the base now refuses as MethodNotFound instead of resting in the
frontier. Widening what the wall can decide is the only move that shrinks the
frontier without fabricating either a success or a refusal.
codex review 45410 then caught that the first peel hand-rolled a SECOND walker
over the refinement shape while this note asserted it was "one traversal
authority, second consumer" — the prose claiming a property the code did not
establish. where_refinement_chain is now the one walk, with exactly two
consumers: predicate collection flat_maps over it, base peeling takes its last
link. The shape test is held once in is_where_refinement_type.
The residue is 13 sites in four shapes, each an upstream receiver-resolution
defect rather than a method-existence fact, and the frontier key now carries the
receiver shape as its third component — so a new call is refused unless it
reproduces the exact unestablished shape the row was measured on. The residual
widening (a second identically-failing call in the same module) is stated in the
note rather than claimed away; closing it needs the content-addressed occurrence
identity the namespace lane is landing.
Verified by execution: two-pass bootstrap + regen_stage0 --verify
(regen_divergence_count=0); the whole dag + src/v2 corpus compiles clean, which
is what proves the 12 peeled sites were DECIDED and not excused (their roster
rows are deleted); the wall witness gains a both-directions RED for the peel and
a control asserting each frontier key component is load-bearing.
Pre-existing and NOT from this PR, reported not fixed:
compiler_tests::rust_btree_set_ord_eligibility_requires_nominal_carrier_shape
fails here and at origin/main — rust_btree_set_element_ord_eligible,
rust_nominal_ord_type_eligible and the test body are all byte-identical to main,
so identical inputs to an identical pure function. The Rust suite was removed
from CI 2026-07-11, which is why it sits unnoticed.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
* WIP: p0 - protect the live system
* Reach the wall from every arm, and judge containers of ground scalars
Two review findings, both verified against the code and both real.
codex review 45430: the method-existence decision lived inline in the FINAL
else of method_pipe_map_keys_values_fallback, so an unresolved map_keys,
sorted_map_keys or map_values whose receiver is not a keyed collection took an
earlier branch and returned recv_rt with an empty diagnostic list — the identical
success-shaped fallback this PR deletes, preserved in the two arms that ran
before it. A wall reachable only from the default arm is not a wall. The
decision is now method_existence_decision, held once and called from all three.
codex review 45398 (second finding): the conformance gate required a plain
shape, so a List is not one, and a declared List<Int> whose body produced a
List<String> was indistinguishable from a conforming declaration. The widening
is the same positive-establishment argument rather than an exception to it — a
container of a ground kernel scalar has no alias, brand, coproduct,
anonymous-literal or cardinality representation standing between the two sides
either, so a difference in the element name is a real difference exactly as a
difference in a scalar name is. Keyed collections are deliberately NOT admitted:
the key and value axes need their own corpus measurement, and assuming the
element argument transfers is the move these notes refuse elsewhere.
Both controls were run against the PRIOR binary rather than reasoned about,
because a predicate that looks discriminating is exactly the artifact that isn't:
List<Int> |> map_keys / |> map_values exit 0 before, 2 located refusals now
fn f() -> List<Int> { ["a","b"] } exit 0 before, 2 located refusals now
Verified by execution: two-pass bootstrap + regen_stage0 --verify
(regen_divergence_count=0); whole dag + src/v2 corpus clean, which is the same
instrument that found the four conformance false-positive classes; both witnesses
green with the new REDs; compiler_tests 30 passed / 1 failed, that one being the
pre-existing rust_btree_set_ord_eligibility failure reported in the previous
commit (byte-identical to origin/main, Rust suite not in CI since 2026-07-11).
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
* WIP: p0 - protect the live system
* WIP: p0 - protect the live system
* Split the residue on a decidable line, and fix the instrument that hid 12 sites
The most transferable finding here is that the INSTRUMENT was wrong before the
wall was. This wall had been measured with `gunbc run --entry
dag/tools/generated_artifact_gate.dag`, which reaches only that gate's import
closure. It reported CLEAN while twelve real sites sat outside it, and they
surfaced from CI instead. The whole-corpus instrument is the compile-clean gate
CI actually runs — `gunbc compile --source-root dag --source-root src/v2
--target dag` — which resolves 1629 sources against 2740 indexed modules. A
narrow instrument reporting clean is indistinguishable from a wall that works.
What the wide instrument found, and what each turned out to be:
TWO REAL DEFECTS, caught by the container widening from the previous commit.
`pure_dag_seam_unreachable() -> Int { 1 / 0 }` is a divergent seam, and the simd
and wgsl FLOAT kernels declared `-> List<Float>` while returning `List<Int>`
from it. The declarations are the correct half — those are float kernels taking
List<Float> arguments. The bodies are unreachable, so nothing ever misbehaved,
which is exactly why this had to be caught by construction rather than by a
consumer. Fixed with a Float projection of the same seam, marked as one
duplication with a bottom-type dissolution trigger: a divergent expression has
no result type to project from, so typing it Int alone was a silent lie
wherever the enclosing declaration was not Int.
EIGHT MORE UNESTABLISHED RECEIVERS, which forced a better model rather than more
roster rows. A receiver with NO AUTHORED NAME is not weak evidence about the
method — it is no evidence about anything, because the receiver's own type was
never established upstream. That is a different judgment failure from "this
receiver has a surface and the method is not on it", so it now gets its own
typed, counted, non-blocking ReceiverTypeUnestablished keyed on the CAUSE (empty
authored name — a decidable test) instead of a row per site. It cannot hide the
case the reviews worried about, because a receiver that DID resolve never
reaches it. That collapsed the roster from six rows to four.
ONE SHAPE NOT FIXED, and the machinery for it deleted. A brand alias can also
arrive as a plain qualified LEAF, Primitive(std.types.NonEmptyStr), rather than
the refinement Conj the peel walks. Three head-resolution strategies were
implemented and measured — lookup_type_for on the node, lookup_type_by_name on
the qualified name, and on its last segment — and none recovered the refinement.
The machinery was deleted rather than shipped unproven, and the site is a
declared row that says plainly that the cause is not yet understood. Unproven
machinery that decides nothing is worse than a declared row that admits what it
cannot decide.
Verified by execution: whole-tree compile-clean 12 blocking diagnostics -> 0,
with 18 ReceiverTypeUnestablished + 4 MethodExistenceFrontierAdmitted counted as
advisories so both classes stay observable; two-pass bootstrap + regen_stage0
--verify (regen_divergence_count=0); compiler_tests 30 passed / 1 failed, that
one the pre-existing rust_btree_set_ord_eligibility failure byte-identical to
origin/main.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
* WIP: p0 - protect the live system
* Pin the ReceiverTypeUnestablished classification, and say what the evidence is
The behavioural evidence for this class is the corpus census — 18 sites
whole-tree, counted as advisories with the compile-clean gate at zero blocking
diagnostics — not a synthetic source. A synthetic reproducer WAS attempted, an
untyped lambda parameter inside a record-field fn, which is the shape the real
sites have; it produced no diagnostic at all, so it did not reproduce the shape
and is not asserted here as though it did. Recording the failed attempt beside
the control, because a witness that quietly asserts something weaker than its
comment claims is the same defect as prose asserting what code does not
establish — the one the reviews caught twice already in this PR.
What the control does pin is the classification, which is the part a later edit
could silently flip in either direction: blocking it fabricates a refusal over
18 correct sites, dropping it restores the #7479 silence. Both directions are
asserted against the three severity partitions directly.
Verified: regen_stage0 --verify (regen_divergence_count=0); wall witness green.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
* WIP: p0 - protect the live system
* Bound the anonymous-receiver admission on the roster (codex review 45459)
The finding is correct and the correction is worth stating precisely, because
the original reasoning was sound about one thing and wrong about another.
When a receiver has NO authored name, the wall cannot tell an existing method
from a nonexistent one — the receiver's own type was never established upstream.
That is true, and it is why refusing the whole class would refuse 18 correct
corpus sites. But it is a fact about DECIDABILITY, and I used it to justify
ADMISSION: every anonymous-receiver call was admitted on the cause alone,
non-blocking, which made every FUTURE such call green including one whose method
does not exist. Unbounded, exactly where existence is unknown. Counting a
diagnostic does not stop invalid code reaching the live system.
The two halves are now separated. The diagnostic still names the real cause —
ReceiverTypeUnestablished says the receiver's type was never established rather
than implying the method is missing, which is the review 45327 lesson. But
admission is gated on the same declared roster as every other unestablished
shape, keyed (module, method, "Primitive()"). The seven measured occurrences are
declared; a new anonymous-receiver call anywhere else REFUSES as
MethodExistenceUndecided. That is a ratchet that can only shrink, and blocking a
new instance of a known deficit class is the factory model, not an
inconvenience.
The gate is already covered by the existing witness: the perturbation loop
asserts, for every one of the 11 rows, that changing the module, the method, or
the receiver shape withdraws the admission.
Verified by execution: whole-tree compile-clean 0 blocking, with 18
ReceiverTypeUnestablished + 4 MethodExistenceFrontierAdmitted counted, so the
roster exactly covers the corpus and nothing is admitted that is not declared;
two-pass bootstrap + regen_stage0 --verify (regen_divergence_count=0);
compiler_tests 30 passed / 1 failed, that one the pre-existing
rust_btree_set_ord_eligibility failure byte-identical to origin/main.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
* WIP: p0 - protect the live system
* Make the frontier a ratchet: declare each row's occurrence count and refuse excess
codex review 45464: the (module, method, receiver_shape) key bounds WHERE an
unresolved call may live but not HOW MANY, so a second call in the same module,
on the same method, failing to resolve the same way, inherited the admission.
That is not hypothetical — the measured rows are not singletons.
v2.compiler.tokenize admits seven `apply`, extdeps.mercurial three `any`,
gunbc.scm_compatibility.mercurial three `map` — so a row admitting seven would
silently admit an eighth.
Each row now declares its measured occurrence count and a per-module fold
refuses the excess with a located, typed FrontierOccurrenceBudgetExceeded. The
comparison is observed > declared, NEVER observed != declared, and that
asymmetry is load-bearing: a narrower compile closure legitimately sees fewer
occurrences, so equality would red any partial build, while fixing a call
legitimately lowers the count and must never red. The budget can only be
exceeded, never undershot — it ratchets down for free and refuses upward
movement.
Why not a stable per-occurrence key, which would close this exactly:
std.occurrence_identity is the corpus authority for the concept, and its own
scope law forbids filename, SourceSpan, authored name, structural Node equality
and content hash as identity inputs, allocating OccurrenceId inside one
graph-scoped allocator. An allocator-assigned integer is not stable across
compiles and so cannot appear as a literal in a declared row. A per-occurrence
key is not merely unimplemented here — it is unavailable from the authority that
owns the concept, which is why the count is the strongest bound the substrate
currently supports. Dissolve-on: content-addressed occurrence identity from the
namespace lane, at which point rows key on the occurrence and the count deletes.
The control is exercised at the mechanism, not through a corpus compile, so the
boundary is exact: declared occurrences pass, declared+1 refuses AND that
refusal blocks, and zero occurrences never red.
On the hand-Rust question raised in review 45469: the cli_run.rs delta is 14
lines, all of them arms of two EXISTING total matches over CompilerDiagnostic,
forced by exhaustiveness once variants are added in .dag — remove them and the
seed does not compile. Hand-written function count is unchanged at 742 before
and after. No new host transport, capability, or carrier.
Verified by execution: whole-tree compile-clean 0 blocking with 18 + 4 counted,
so declared counts equal observed exactly; two-pass bootstrap + regen_stage0
--verify (regen_divergence_count=0); compiler_tests 30 passed / 1 failed, that
one the pre-existing rust_btree_set_ord_eligibility failure byte-identical to
origin/main.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
* WIP: p0 - protect the live system
* Check every explicit return against the declared type (codex review 45472)
Verified before fixing, and the finding was exactly right:
fn f(cond: Bool) -> Int { if cond { return "wrong" } 1 } exit 0
The wall compared only the body's FINAL inferred type. The block's value is the
trailing 1, which conforms, so the wrong-typed early exit was never compared
against anything. An early return is a second exit from the same declaration and
must meet the same declared type.
The first attempt threaded the check onto the `expected` already flowing into the
ExprReturn arm, and it did NOT work — measured, not assumed: a return inside a
statement-position `if` carries no expected type, so the probe still compiled
clean. Threading a declared-return field through InferScope would have reached
it, but that is ~14 construction sites across three files including the emitter.
The check is instead a post-pass at infer_item, which is local, needs no scope
change, and reuses declared_type_conformance_diags rather than minting a second
relation — so an early exit is judged by exactly the ground-kernel-scalar and
ground-element-collection discipline the trailing expression is judged by, and
widens with that gate rather than beside it.
Verified by execution: the probe above now refuses with a located
`expected 'Primitive(Int)', got 'Primitive(String)'`; whole-tree compile-clean
still 0 blocking, so no legitimate early return in the corpus reds; two-pass
bootstrap + regen_stage0 --verify (regen_divergence_count=0).
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
* Hold the frontier-occurrence key in the diagnostic authority (codex review 45476)
The occurrence-budget fold hand-rolled a match over CompilerDiagnostic inside
v1.compiler.infer, which put a second reader of the coproduct outside the
coproduct's own authority: adding a variant could leave the budget silently
blind to it, and two places would decide what a diagnostic means.
diagnostic_frontier_occurrence_key now lives in 00_core beside diagnostic_to_span
and diagnostic_to_message, and the budget consumes it. Only two variants carry an
occurrence against a row — MethodExistenceFrontierAdmitted names its receiver
shape directly, and ReceiverTypeUnestablished always arises from a receiver with
no authored name, whose shape renders as Primitive(), which is why that literal
is the key rather than a field on the variant. A new variant that should be
budgeted is added in that one fn, next to the variants it joins.
Verified by execution: whole-tree compile-clean 0 blocking with 18 + 4 counted,
unchanged, so the routing is behaviour-preserving; two-pass bootstrap +
regen_stage0 --verify (regen_divergence_count=0); compiler_tests 30 passed /
1 failed, the pre-existing rust_btree_set_ord_eligibility failure.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
* WIP: p0 - protect the live system
* Stop the return walk at lambda boundaries, and give the seed projection its receipt
codex review 45481, finding 1 — confirmed by execution before fixing:
fn apply_it(g: fn(Int) -> String, v: Int) -> String { g(v) }
fn outer(v: Int) -> Int { apply_it(g: x => { return "inner" }, v: v) 1 }
-> expected 'Primitive(Int)', got 'Primitive(String)'
collect_explicit_return_types recursed through ExprLambda, so a return belonging
to the LAMBDA's callable return type was checked against the enclosing
declaration. That is a fabricated refusal — the mirror image of the hole the walk
was added to close, and §5 forbids one exactly as it forbids the other. Every
callable boundary is a new declaration and its returns are judged against it. The
walk now stops at ExprLambda, which also means lambda returns are not yet judged
at all; that narrowing is stated on the note rather than implied, and it
dissolves when the walk carries each callable's own declared return.
The discriminating PAIR is now witnessed, since one direction alone proves
nothing here: the early return must refuse AND the lambda return must not.
codex reviews 45469/45481/45484, hand-Rust gate — receipt added in the gate's own
form, both on the carrier (v1.compiler.core compiler_diagnostic_seed_projection_note,
beside the coproduct whose extension forces the arms) and in the changed planning
artifact. It is an explicit deferral naming lane
(compiler-static-failure-closure) and ROADMAP row (hand-MAINTAINED Rust -> zero
at v2 self-host), with the argument that an exhaustiveness arm is a different
class from the gate's usual subject: the gate's other deferrals are decision
surfaces that COULD live in .dag and therefore owe their own schedule, while an
arm cannot live anywhere but the seed's projection of the coproduct and
disappears exactly when the seed does.
Checkable receipt: hand-written fn count in cli_run.rs is 742 at origin/main and
742 here; the diff is 13 added lines with zero `fn`. The 322 lines review 45484
attributes to hand-Rust in compiler_tests.rs are not hand-written at all — that
file is GENERATED, listed in gunbc.stage0_emit_model.generated_stage0_files and
emitted by regen_stage0 from src/v1/compiler_tests_rust.dag, so its growth is
witness text authored in .dag.
Verified by execution: both probes correct in both directions; whole-tree
compile-clean 0 blocking; two-pass bootstrap + regen_stage0 --verify
(regen_divergence_count=0); compiler_tests 30 passed / 1 failed, the pre-existing
rust_btree_set_ord_eligibility failure.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
* chore: regenerate drifted generated artifacts (ci auto-heal)
* WIP: p0 - protect the live system
* Make the budget a real ratchet, fix the witness arity, and make the seam diverge
Three findings, all correct, and one of them was mine to catch before review.
cursor review 45494 finding 2 — THE WITNESS DID NOT COMPILE. I changed
frontier_occurrence_budget_diags to take a locating module_span and did not
re-run the suite, so three call sites in the witness still passed two arguments.
Reading caught what I skipped running; the run would have caught it immediately
and I did not do the run. Fixed, and the suite is green again.
codex review 45491 — the ceiling did not ratchet. `observed > declared` let
seven shrink to six while the declared seven stood, so a seventh call could
return silently: a static limit, not a ratchet, and the note claimed the ratchet
anyway. My stated justification for the ceiling — that a narrower closure sees
fewer occurrences — was simply wrong about this check, which runs per MODULE:
every occurrence of a module's rows is present whenever that module is
typechecked at all, and a closure omitting the module never runs its rows. So
there was no partial-visibility case to protect and the asymmetry bought
nothing. The comparison is now equality, which removes the headroom a
reintroduction slips into: fixing a call reds until the declared count is
lowered. Both directions are asserted in the witness, since the under-count half
is what makes it a ratchet and is the half an author is tempted to relax.
cursor review 45494 finding 1 also flagged the equality as contradicting the
note. It contradicted the note because the note was stale, not because the code
was wrong — the note has been rewritten to describe what the code does and to
record why the ceiling reasoning failed.
codex review 45493 — `1.0 / 0.0` IS NOT DIVERGENT. Under IEEE-754 it is positive
infinity, not a trap, so the Float seam RETURNED and the kernels asserted
unreachable would have produced [+inf]. A fabricated plausible output, the exact
thing §5 forbids, introduced while fixing a different fabrication. Integer
division by zero traps; float division by zero does not, however similar they
look. The Float projection now forces the Int seam to evaluate in its condition,
so divergence happens before any Float is produced. Confirmed in the emitted
Rust: `if (pure_dag_seam_unreachable() == 0)` over `pub fn
pure_dag_seam_unreachable() -> i64 { (1 / 0) }`.
Verified by execution: two-pass bootstrap + regen_stage0 --verify
(regen_divergence_count=0); whole-tree compile-clean 0 blocking; compiler_tests
30 passed / 1 failed, that one the pre-existing rust_btree_set_ord_eligibility
failure byte-identical to origin/main.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
* WIP: p0 - protect the live system
* Count the unjudged conformance residue, and author the receipt where it survives
codex review 45500 — the conformance wall's unjudged branch returned an empty
diagnostic list, so an unproven declaration was byte-for-byte indistinguishable
in the output from a proven-conforming one: the absence of a check reading as
the presence of a proof. It now emits DeclaredTypeConformanceUnjudged, counted
and non-blocking, so the wall's frontier has a SIZE — 3005 declarations
whole-tree — a number that falls as the relation widens and is therefore a
prioritizable measure of the gap rather than an invisible one.
It fires only where the declared and produced SHAPES DIFFER. Identical shapes
have nothing to prove, and counting them would bury the signal under
declarations nobody doubts; the residue that matters is exactly the set where a
mismatch could hide.
codex review 45501 finding 2 — the HAND-RUST receipt had gone stale, reading
five variants and 13 lines after a sixth variant landed. That made the receipt
itself the stale-prose defect it exists to prevent. Corrected to six variants
and 18 lines, with both figures now marked as re-derived from their two commands
on every variant addition rather than carried forward.
AND THE RECEIPT WAS IN THE WRONG FILE, which is why it vanished: I had written it
into docs/plans/compile-clean-forcecheck.md, and that .md is a GENERATED
PROJECTION of dag/gunbc/plans/compile_clean_forcecheck.dag — the CI auto-heal
commit regenerated the doc and silently reverted it. The receipt is now authored
in the .dag plan authority and survives the heal, which is verified by running
the generated-artifact gate and seeing the text reappear in the projection. The
plan carrier says so in-place, so the next author does not repeat it.
review 45499 — the count/length pair on the algebra templates is a §3 nicknaming
fork RECORDED rather than introduced, and the row now says so. The fork's
authority is the interpreter, which dispatches length, count and size to one
native arm and predates this change; the templates listed only length, so
`String |> count` resolved at runtime with no declared row, which the
method-existence wall exposed the moment it began proving absence from the
roster. Reconciling the declaration to the runtime is the honest direction —
inventing a distinct meaning for count would be the fabrication, and dropping the
row would refuse a working call. Dissolve-on: one name across the interpreter
arm, the templates, and the corpus, which is a corpus-wide rename and its own
lane.
Verified by execution: whole-tree compile-clean 0 blocking; two-pass bootstrap +
regen_stage0 --verify (regen_divergence_count=0); generated-artifact gate green
with the receipt present in the projection; compiler_tests 30 passed / 1 failed,
the pre-existing rust_btree_set_ord_eligibility failure.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
* WIP: p0 - protect the live system
* WIP: p0 - protect the live system
* Ground filesystem_read's return type; count the residue the gate was not counting
CI red on the last push was my own wall firing on a site my instrument never
reached, and chasing it found three defects underneath it.
ROOT CAUSE. filesystem_read was registered in 04_method as a bare
type_variable_node, so `filesystem_read(path: p).content` established nothing:
the field lookup had nothing to look in and the result was a fabricated
Primitive() carrying no name. A later `.split` on that value was then accepted
with no judgment behind it — #7479's exact shape one layer down, surviving
because the interpreter dispatches split on the native String regardless, so
nothing ever failed loudly. The return type was never unknown: runtime_rust.dag
already emits `pub struct FilesystemReadResult { pub content: String }`.
Declaring it makes the seed's struct and the compiler's type one fact instead of
two, via a make_kernel_record_type helper that builds the same
Conj-with-named-children shape lookup_field_type_node already walks for authored
records — so the kernel path and the authored path cannot drift.
WHY MY INSTRUMENT MISSED IT, WHICH IS THE MORE USEFUL FINDING. Whole-tree
compile-clean reported zero blocking while this site sat outside its closure;
the discovery corpus resolves entries compile-clean never opens. That is the
SECOND time this lane's instrument was narrower than the wall it was measuring —
the first was main_wet hiding twelve sites. The measurement was wrong before the
wall was, both times.
THE RESIDUE WAS NOT ACTUALLY COUNTED. compile_clean_diagnostic_is_advisory is a
CLOSED ALLOWLIST, not the complement of is_hard, so all three non-blocking
variants this lane adds matched neither predicate: they rendered to the terminal
while every count the gate reported read zero for them. I had been telling
reviewers the frontier was counted, and the population figures I quoted came
from grepping log text — no mechanism in the repository counted them. Found by
executing the gate before and after the expansion fix and seeing its advisory
total sit unchanged at 4590 while the printed population halved. The three
variants are now in the allowlist; the total moves 4590 -> 6176 and nothing
falls through either counter.
THE FRONTIER WAS REPORTED AT NEARLY TWICE ITS SIZE. Measured, 1436 of the 3005
unjudged conformance pairs were one type compared against ITSELF at two
expansion depths — a declaration naming T against a body producing T's expanded
body (203 Node, 173 Outcome, 46 Witness, 43 Optional, 38 PipelineStep, long
tail). Resolving each side through lookup_type_for before comparing is a real
judgment step, not a name heuristic, and it can only remove a diagnostic since
both branches already treated unequal shapes as unjudged rather than as a
refusal. 3005 -> 1566. An inflated frontier is not a conservative error: it
buries the residue that genuinely cannot be decided under pairs never in doubt.
What remains is meaningful and independently rediscovers DESIGN's own open
threads — Nat vs Int (61), Hash vs ContentHash (29), brand aliases like
NonEmptyStr vs String (207), anonymous record literals (150+).
codex review 45533 finding 2 — every explicit-return diagnostic reported
body_typed.span, so a function with several early returns pointed them all at
one location. The collector now carries each return VALUE rather than only its
type, and each refusal is located at the return that caused it.
The two frontier rows for language_source_scaffold_index_test are deleted: they
were this same filesystem_read gap, and the cause I authored for them ("an
untyped lambda parameter") was a guess that was simply wrong. The occurrence
ratchet then fired in the FALLING direction and its message asserted a new call
had appeared — a diagnostic claiming a direction it had not measured. Reworded
to state both directions and to say which remedy each one implies.
Receipt figures re-derived, and one of them had never been reproducible: the
claimed 742 hand-written fns in cli_run.rs matches no command — 501 bare `fn`,
245 `pub fn`, never 742. Every figure now names the command that produces it:
`grep -cE '^(pub )?fn '` is 746 on main and 746 here (flat), the diff is 28
added / 0 removed, and zero added lines declare a fn.
Verified by execution: whole-tree compile-clean 0 blocking with 0 diagnostics
falling outside both counters; the #7479 repro still refuses with zero files
emitted while the `map` control still compiles clean; both CI-red sites now
green; two-pass regen + regen_stage0 --verify (regen_divergence_count=0);
compiler_tests 30 passed / 1 failed, that one being
rust_btree_set_ord_eligibility_requires_nominal_carrier_shape, whose three
functions and test body are byte-identical to origin/main.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
* WIP: p0 - protect the live system
* Stop keeping two copies of one receipt
review 45565 quoted the HAND-RUST receipt back as "742 -> 742, +18 lines" after
those figures had already been re-derived to 746/746 and 28 lines. Nothing was
stale in the sense of nobody updating it: the receipt existed in TWO carriers,
and I re-derived it in one.
The forked paragraph's own next sentence already named the carrier as the single
authority for this receipt, and then restated the numbers anyway — §3 doing
exactly what §3 says it does, inside a single paragraph. A receipt duplicated
across two carriers is worse than one kept in the wrong place: both read as
authoritative, they diverge silently, and a reviewer is as likely to cite the
stale copy as the live one. That is not hypothetical here; it is what happened.
So the plan carrier no longer repeats the figures. It states the claim the
receipt makes — the hand-Rust carrier census is flat, only arm count moved — and
points at the one place the numbers live, beside the coproduct whose extension
forces the arms, where each is stated with the exact command that reproduces it.
A reader checks by running those commands rather than by trusting either copy.
The paragraph says why it is written that way, so the copy does not grow back.
The projection was regenerated through main_wet on the generated-artifact gate,
which then re-runs clean; the doc is a projection and re-authoring it directly
is reverted by the heal.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
* Record why the seed reads Node storage directly, since the answer is not per-function
review 45570 asks that is_where_refinement_type and where_refinement_chain route
through a canonical query/fold surface, or carry a bounded disposition with
owner, lane and trigger. Measured, neither is available in the shape asked for,
and the reason is worth writing down where the next reader hits it.
There is no canonical surface reachable from here. fold_node and node_query live
in src/v2/std; no v1 seed module imports v2 at all; and v1 COMPILES v2, so
routing v1 inference through v2's fold inverts the bootstrap rather than tidying
it. DESIGN's fold_node line is scoped to the 7 v2 stages — a DRY example within
v2, not a rule binding the seed.
And the disposition is the seed's, not these functions'. They are 2 of 589
direct Node-storage reads in this file, 579 of which are on origin/main: the
seed IS the traversal, the stage that walks the tree so later stages need not.
Attaching a per-function trigger to 2 reads while 587 identical reads beside
them carry none would describe separable work that does not exist — a fabricated
bound, which is the same defect as a fabricated refusal pointed at a schedule.
The real trigger is the one the hand-Rust receipt already carries: the v1 seed
shrinks to zero at v2 self-host and these dissolve with it.
Worth noting that where_refinement_chain exists BECAUSE review 45410 asked for
exactly this consolidation — it is the single traversal authority that replaced
two independently-drifting walkers.
Verified: two-pass regen + regen_stage0 --verify (regen_divergence_count=0);
whole-tree compile-clean 0 blocking, 6176 advisory, 0 diagnostics outside both
counters.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
* WIP: p0 - protect the live system
* State the return walker's disposition where it was asked, not only on its sibling
review 45580 raises the walker question again, this time against
collect_explicit_return_values. The DESIGN citation is the same one review 45570
made and I answered: node_query appears zero times in DESIGN, the single
fold_node line is scoped to the 7 v2 stages, fold_node/node_query are v2
substrate, no v1 seed module imports v2, and v1 COMPILES v2 — so routing seed
inference through v2's fold inverts the bootstrap rather than tidying it.
But one part of the finding is fair and is the reason it had to be found twice.
I recorded that reasoning on where_refinement_receiver_peel_note and left
explicit_return_conformance_note carrying only its lambda-coverage trigger, so
the note nearest the walker said nothing about the walker. A disposition stated
on one carrier and omitted from its sibling is not stated. It is now on both.
Measured, so the claim is checkable rather than asserted: self-recursive
`children |> flat_map` collection is the v1 seed's only traversal idiom — 16
such sites on origin/main across 04_emit_info, 04_sigs, 04_infer, 05_emit,
05_emit_rust, compile and complexity. There is no shared v1 walker to route
through because each collector recurses itself. This is the 17th instance of a
16-instance idiom, and its trigger is the one every sibling carries: the v1 seed
shrinks to zero at v2 self-host and they dissolve together.
Generalizing a shared collector for this one call site would ADD a 17th shape
rather than remove one, and attaching a per-function owner/lane/trigger to it
while 16 identical siblings carry none would describe separable work that does
not exist — the same fabricated bound I declined at review 45570.
Verified: two-pass regen + regen_stage0 --verify (regen_divergence_count=0);
whole-tree compile-clean 0 blocking.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
* Judge conformance with the structural relation, not a rendered shape string
codex review 45600 — the not-both-ground branch compared node_type_shape OUTPUT
and treated equality as proven conformance. That projection is lossy by design:
it renders every anonymous product as the literal text Product(<anon>) and every
named product as its OUTER NAME ONLY, discarding fields, variants and their
types. So two structurally different records compared EQUAL and were stamped
proven-conforming, and distinct definitions sharing an outer name did the same.
That is the exact fail-open this wall exists to delete, reintroduced while
removing a different one, and by the same mechanism as the 1.0/0.0 seam earlier
in this PR: a projection that LOOKS like evidence used where a proof was
required. A display projection belongs in a message; a judgment must consume the
structural relation. The finding is correct and the defect was mine — it arrived
with the expansion-depth fix two commits ago.
conformance_expanded_node now returns the resolved, brand-peeled NODE and the
branch calls node_type_compatible on it, which recurses into container elements
and compares canonical template names, so identity is established rather than
rendered. Its known imprecision is safe in exactly this position: it reports
mismatch for four classes of correct code, and a mismatch here yields the counted
unjudged advisory rather than a refusal, so a false negative costs a count and
never reds correct code. The wrong direction would have been to keep the string
because it was quieter.
The peel rides the SAME authority the method wall uses
(peel_where_refinement_base), one traversal with two consumers rather than a
second minted here, which also grounds the brand-alias class that dominated the
residue: 1566 -> 1024.
On review 45593, which asked that the unjudged branch refuse or be bounded by an
explicitly admitted frontier: I measured the frontier before answering, and a
roster is the wrong shape here — the residue is 398 DISTINCT declared/produced
pairs with 242 occurring exactly once, a long tail that grows with the corpus
rather than a small admitted set. Refusing it outright is also not available:
the classes are brand aliases, anonymous record literals, the Nat/Int fork and
unsubstituted generics, all of them CORRECT code, so refusal would red ~1000
sound declarations and fabricate refusals at scale. What was actually available
was to shrink it by judging more, which is what this commit does — and the
lossy-string defect 45600 found was sitting inside the previous attempt to do
exactly that.
Verified by execution: whole-tree compile-clean 0 blocking, 5634 advisory, 0
diagnostics outside both counters; conformance RED control refuses all four
shapes (scalar return, list element, data init, early return) each located;
#7479 still refuses with zero files emitted and the map control still compiles
clean; regen_stage0 --verify (regen_divergence_count=0); compiler_tests 30
passed / 1 failed, the pre-existing rust_btree_set_ord_eligibility failure whose
functions and test body are byte-identical to origin/main.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
* WIP: p0 - protect the live system
* Record the proven conformance hole and the 🟡 seed-traversal frontier
Two reviews, and the first one is a finding I could not close.
review 45647 is CORRECT and I proved it by execution before answering: the
unjudged branch is not merely unmeasured, it lets a program that is simply WRONG
reach emission. `type R { x: Int }` `type S { y: String }`
`fn wrong_record() -> R { S { y: "a" } }` compiled EXIT 0 and EMITTED TWO FILES
while reporting the mismatch as a counted advisory. Two structurally unrelated
named records is not a representation gap; it is the conformance half of #7479.
I ATTEMPTED THE FIX AND IT IS NOT LANDED. Three successive narrowings of a
refuse-when-both-sides-are-named-structured rule, each measured against the whole
corpus: (1) structured and named -> 90 refusals of CORRECT code, dominated by the
two-representation optionality class; (2) narrowed to inhabited named records
with kernel scope names excluded -> 15; (3) additionally guarding the raw nodes
-> 27, by which point the population had shifted to a NEW class, produced sides
that are let-BINDING names rather than types. 90 -> 15 -> 27 is the finding: each
guard displaces the false-positive population instead of shrinking it. That is
the exemption-accumulation this wall refuses elsewhere, and shipping any of the
three would red correct code.
So the arm is reverted and the hole is recorded on the carrier with its executed
witness, the three measured attempts, the named blocking obstacle, and a
dissolution trigger. The obstacle is not vague: the produced-side node reaching
this branch is not reliably a TYPE — it can be a nominal reference, a kernel
encoding of cardinality or absence, an anonymous literal, or a let-binding
identity — so no predicate over its shape separates a real mismatch from a
representation gap until produced-side type identity is established upstream.
Dissolve-on: feature:conformance-produced-type-identity. My own note's line
applies to me here: unproven machinery that decides nothing is worse than a
declared row that admits what it cannot decide.
reviews 45570 / 45580 / 45666 — the walker. 45666's sharpest point is right and
I had leaned on the weak form: sibling count is PRECEDENT, and precedent is debt,
not permission. The justification is reachability, not popularity — fold_node and
node_query are v2 substrate, no v1 seed module imports v2, v1 COMPILES v2 so
routing seed inference through v2's fold inverts the bootstrap, and no shared v1
walker exists because every v1 collector recurses itself. The review also asked
for the repo's own declared-scaffold form rather than prose, which is a fair and
concrete ask: seed_node_traversal_frontier is now a 🟡 dissolve-on row covering
the CLASS (16 sibling sites on main, 579 direct field reads in 04_infer alone),
with the cost of closing now and the same trigger the hand-Rust receipt carries,
because it is the same seed and the same endpoint.
Verified: two-pass regen + regen_stage0 --verify (regen_divergence_count=0);
whole-tree compile-clean 0 blocking, 5637 advisory, 1024 counted residue, 0
outside both counters; #7479 refuses with zero files emitted; conformance RED
control refuses all four shapes.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
* WIP: p0 - protect the live system
* Prove the permission is main's, not this path's
codex review 45695 holds that the PR "knowingly leaves a demonstrated wrong
program able to reach emission through the newly added conformance path" and
that the identity work must land before this path may permit emission. The hole
is real — I proved it last commit. The attribution is not, and it decides the
sequencing question, so I measured it instead of arguing it.
The identical program built against origin/main:
exit=0 files emitted=2 diagnostics=0
On this branch: the same 2 files, plus one counted advisory naming the mismatch.
The conformance path does not newly PERMIT that emission; main permits it
silently and this branch makes it visible and countable. Blocking here would
hold back the method-existence wall — which does refuse, and emits nothing — and
leave the live system strictly less protected than landing it.
A fourth fix attempt isolated the obstacle exactly rather than leaving it
inferred. Guarding on "both sides are Conj whose authored name resolves via
lookup_type_by_name to a record declaration" still refused 14 seed sites, and
every one had a LET-BINDING name on the produced side (module_emit_scope,
scope_after_expr, lookup_item, service_fallback_transport). lookup_type_by_name
resolves those because bindings and types inhabit ONE name environment, so the
guard cannot distinguish a type identity from a binding identity. That is the
recorded obstacle, now demonstrated: no predicate over the produced node's shape
or name can close this class, which is why four attempts moved the false-positive
population (90 -> 15 -> 27 -> 14) instead of shrinking it.
Attempt 4 is reverted like the other three. The row now carries the main
comparison alongside the witness, the four attempts and the trigger.
Verified: two-pass regen + regen_stage0 --verify (regen_divergence_count=0);
whole-tree compile-clean 0 blocking.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
* WIP: p0 - protect the live system
* Fix list_append call labels that main's call-shape wall refuses
The floor failed on src/v2/test/claim/bash_program_fold_support.dag with eight
"call shape mismatch calling 'list_append': no parameter named 'xs'" refusals.
Not this lane's code: the file is byte-identical to origin/main and no commit
here touches it. It is main's own #7519 call-shape wall firing on a call site
that predates it — list_append is declared (left, right) in v2.std.algebra and
this file passed xs:/ys:, which the wall now correctly refuses and which was
silently accepted before it existed. Exactly the fail-open class #7519 closes.
It surfaced here rather than on #7519 because the two runs have different reach:
a PR-scoped compile-clean does not open test entrie…
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Follow-up to #7470, working both rounds of its review. Two commits.
run_stageis deliberately not here — the review ordered carrier hardening first, and its ownrun_stageprerequisite (retaining the full resource profile on the parsedRunnable) is a separate change.The defect this PR hit, and what it says
The first head failed the CI floor:
Moving
FloorFinalizationout of theWalkFinalizationsum into a standalone record changed its runtime shape fromValue::VarianttoValue::Record, and the executor's parser only matched variants. Every.dagwitness stayed green throughout, because field access works fine on a record — the parser itself was never executed against the new shape. Specification-without-execution, on my own change.Both shapes are matched now, by type name rather than by "has a field called
declared_resolve_count" (which would admit any record carrying one). Proven by runningclaim_executoragainst the budget RED-control fixture, which is what that fixture exists for:1. Parameterized
WalkPlan, and the wall that isn't thereThe floor plan returns a plan parameterized on
FloorFinalization; regen, plan-artifact and falsifier onNoWalkFinalization.FloorFinalizationmoves out ofstd.realization_scheduleintogunbc.ci_materialization, beside the count it is about, so the generic carrier stops owning a growing coproduct of gunbc-specific receipt policies.declared_resolve_countisNat.The review asked for this as a construction wall. It is not one. Probed by execution: substituting the empty policy into the floor while leaving the signature unchanged typechecks, and fails only at the first field access. A narrower probe isolates the general defect:
expected 'Primitive(Int)', got 'Primitive(String)')fn f() -> Intreturning a string typechecksdataannotation vs valuedata d: Intbound to a string typechecksSo: §5 wall-after-grounding. The parameterization declares the intended family and removes the std-level fork; the enrolled value witnesses and the runtime parser are what actually refuse, until return-position typechecking lands. All five in-tree notes that claimed otherwise now say this —
floor_finalization_note,walk_plan_uniformity_note, the RED fixture note, and two seed doc comments.2.
require_materialization_disclosure: BooldeletedIts
falsearm returned before the materialization check while the success line — unconditional on the Bool — still reported that disclosure held. A writable bypass with a lie attached, pre-authored for a consumer that does not exist.3. Finalization witnesses
floor_plan_projects_the_declared_resolve_count_authorityplus a forked-count RED, and the three no-finalization rows (regen / plan-artifact / falsifier). I initially omitted those three as tautologies; that reasoning assumed the declared return type bounds the runtime value, and the probe above shows it does not — so matching the actual value is load-bearing, not a match over a one-inhabitant type. Corrected.4. Attempt subject hardening
WalkAttemptId— aPathSegmentbrand with one constructor, testingstd.types.path_segment_is_safe.../other-attempt,a/b,.,.., backslash, CR, LF and NUL refuse through both producers. std holds the law as a predicate; each brand constructs itself through it.pr_number: none; that conflation is now three named states (WirePrAbsent | WirePrPresent | WirePrMalformed).tested_head_shawas carried and never read, so a receipt could restate which subject it certified and be believed. Three bindings precede any freshness question; a mismatch isMergeDeniedSubjectMismatch, its own state.git_sha1_object_id/git_sha256_object_idland besideGitObjectIdinextdeps.git.object_store, checking exact length (40/64) and canonical lowercase hex through the existinggit_decode_lower_hex_octetsrather than a second hex reader. Before this,sha1:x,sha1:not-hexand a 64-digit value labelledsha1all parsed — family without length and syntax is not identification.git_object_id_eqmoved there too; holding generic Git behaviour in the admission consumer was a fork.23 witnesses green, including path-traversal, line-terminator, trailing-line, malformed-PR and seven object-id validation REDs.
5. Emitter: CR has never been escaped — and the first fix was only half
escape_string_literal_bodysplit on the delimiter"\r", but this language's tokenizer has no\rescape (its table is\" \\ \n \t \{ \}and\xHH), so that delimiter was the two characters backslash andr. The emitted seed reads.split(&"\\r")…join(&"\\r")— a no-op. Carriage returns have passed through unescaped into every emitted target for as long as the function has existed, dead only because no corpus string carried one. The first that did turned it into a hard emit failure.Fixing the delimiter was half. The replacement was briefly
\rand\0— Rust-shaped, in a target-independent function:emit_string_literalinvokes it for Rust, Dag, Go and Python alike and never sees aRenderTarget, so\rinto a Dag literal reproduces the exact backslash-r bug just closed. The spelling is\x0d/\x00, the hex form all four grammars accept.Proven by an inverse-pair round trip through the tokenizer's own
process_escapes, with a control asserting the characters are actually replaced (identity round-trips perfectly). Rust is proven by compilation. Go and Python are not proven and the test says so — no toolchain here, no modeled escape grammar for either target; dissolve-on named.6. Residue cleaned
The duplicate
MergeDeniedWrongAttemptarm, and the duplicateMergeDeniedSubjectMismatcharm the mechanical pass that added the new variant reintroduced. Stale diagnostics: finalization described as "read from the plan closure at arm time"; the strict-parser diagnostic omitting thefinalizationfield. A resolve-count mismatch now locates itself at<entry>::<function>plus the field it consumed, rather than always pointing at the production authority.Not here
run_stage— needs the review's own prerequisite first (retainspawns_host_compilerand the memory class on the parsedRunnable). Written and stashed; next PR..dagwitness — mechanically available, but it adds a cold entry-closure resolve and so bumpsci_floor_declared_resolve_countfrom 1 to 2, which that gate's own note requires be raised consciously by an operator-signed line. Left as a native test; flagging the decision rather than taking it.Pre-existing, not caused by this PR
cargo buildfails on thev1-stage0-std-corecrate at this branch's merge base too (7 errors, unresolvedextdeps_units_*/std_occurrence_identityimports). CI'sbuildjob does not compile that crate.compiler_tests::rust_btree_set_ord_eligibility_requires_nominal_carrier_shapewas already red before these changes.Verification
cargo fmt --all --checkclean ·cargo test --bin claim_executor floor_finalization2 passed · 23 attempt witnesses green · 5 finalization witnesses green · 2 native escape round-trip tests green · enforcement + actuator suites green ·regen_stage0a fixed point over consecutive runs · executor parse proven end-to-end against the RED-control fixture.Draft pending the fleet floor on this head.
🤖 Generated with Claude Code
https://claude.ai/code/session_01N7LfCpidMuDjV3FxYUHv1K